Nuprl Definition : R-Feasible
11,40
postcript
pdf
R-Feasible{i:l}
R-Feasible
(
R
)
== es_realizer_ind(
R
;
== es_realizer_ind(
True;
== es_realizer_ind(
left
,
right
,
rec1
,
rec2
.(
rec1
rec2
R-compat{i:l}(
left
;
right
));
== es_realizer_ind(
loc
,
T
,
x
,
v
.True;
== es_realizer_ind(
loc
,
T
,
x
,
L
.normal-type{i:l}
== es_realizer_ind(
loc
,
T
,
x
,
L
.normal-type
(
T
);
== es_realizer_ind(
lnk
,
tag
,
L
.True;
== es_realizer_ind(
loc
,
ds
,
knd
,
T
,
x
,
f
.((normal-ds{i:l}(
ds
)
normal-type{i:l}(
T
))
== es_realizer_ind(
((
isrcv(
knd
))
(
loc
= destination(lnk(
knd
)))));
== es_realizer_ind(
ds
,
knd
,
T
,
l
,
dt
,
g
.(((
isrcv(
knd
))
== es_realizer_ind(
ds
,
knd
,
T
,
l
,
dt
,
g
.(
(((
eq_lnk(lnk(
knd
);
l
))
== es_realizer_ind(
ds
,
knd
,
T
,
l
,
dt
,
g
.(
(
T
= fpf-cap(
dt
; id-deq; tag(
knd
); void)))
== es_realizer_ind(
ds
,
knd
,
T
,
l
,
dt
,
g
.(
(destination(lnk(
knd
)) = source(
l
))))
== es_realizer_ind(
(normal-type{i:l}(
T
)
normal-ds{i:l}(
ds
))
== es_realizer_ind(
normal-ds{i:l}
== es_realizer_ind(
normal-ds
(
dt
));
== es_realizer_ind(
loc
,
ds
,
a
,
T
,
P
.normal-ds{i:l}
== es_realizer_ind(
loc
,
ds
,
a
,
T
,
P
.normal-ds
(
ds
);
== es_realizer_ind(
loc
,
k
,
L
.True;
== es_realizer_ind(
loc
,
k
,
L
.True;
== es_realizer_ind(
loc
,
x
,
L
.True)
latex
clarification:
R-Feasible{i:l}
R-Feasible
(
R
)
== es_realizer_ind(
R
;
== es_realizer_ind(
True;
== es_realizer_ind(
left
,
right
,
rec1
,
rec2
.(
rec1
rec2
R-compat{i:l}(
left
;
right
));
== es_realizer_ind(
loc
,
T
,
x
,
v
.True;
== es_realizer_ind(
loc
,
T
,
x
,
L
.normal-type{i:l}
== es_realizer_ind(
loc
,
T
,
x
,
L
.normal-type
(
T
);
== es_realizer_ind(
lnk
,
tag
,
L
.True;
== es_realizer_ind(
loc
,
ds
,
knd
,
T
,
x
,
f
.((normal-ds{i:l}(
ds
)
normal-type{i:l}(
T
))
== es_realizer_ind(
((
isrcv(
knd
))
(
loc
= destination(lnk(
knd
))
Id)));
== es_realizer_ind(
ds
,
knd
,
T
,
l
,
dt
,
g
.(((
isrcv(
knd
))
== es_realizer_ind(
ds
,
knd
,
T
,
l
,
dt
,
g
.(
(((
eq_lnk(lnk(
knd
);
l
))
== es_realizer_ind(
ds
,
knd
,
T
,
l
,
dt
,
g
.(
(
T
= fpf-cap(
dt
; id-deq; tag(
knd
); void)
Type{i}))
== es_realizer_ind(
ds
,
knd
,
T
,
l
,
dt
,
g
.(
(destination(lnk(
knd
)) = source(
l
)
Id)))
== es_realizer_ind(
(normal-type{i:l}(
T
)
normal-ds{i:l}(
ds
))
== es_realizer_ind(
normal-ds{i:l}
== es_realizer_ind(
normal-ds
(
dt
));
== es_realizer_ind(
loc
,
ds
,
a
,
T
,
P
.normal-ds{i:l}
== es_realizer_ind(
loc
,
ds
,
a
,
T
,
P
.normal-ds
(
ds
);
== es_realizer_ind(
loc
,
k
,
L
.True;
== es_realizer_ind(
loc
,
k
,
L
.True;
== es_realizer_ind(
loc
,
x
,
L
.True)
latex
Definitions
es
realizer
ind
,
R-compat{i:l}(
A
;
B
)
,
isrcv(
k
)
,
P
Q
,
b
,
eq_lnk(
a
;
b
)
,
Type
,
fpf-cap(
f
;
eq
;
x
;
z
)
,
id-deq
,
tag(
k
)
,
void
,
s
=
t
,
Id
,
destination(
l
)
,
lnk(
k
)
,
source(
l
)
,
P
Q
,
normal-type{i:l}(
T
)
,
normal-ds{i:l}(
ds
)
,
True
FDL editor aliases
R-Feasible
origin